#include"cdcl.h"
#include<stdlib.h>
#include <stdio.h>
#include "myqueue.h"
dpllresult* CDCLalgorithm(cdcl* _cdcl);
extern int max_var_id;
//#define RANKPRINTF(rank, format, args...)   printf(format, ##args); printf("\n"); fflush(stdout)

#define RANKPRINTF(rank, format, args...)  printf("[RANK %d] ", rank); printf(format, ##args); printf("\n"); fflush(stdout)

//DGliteral* parentdecision;
//DGraph* dependence_graph;

/**
 * Helper function to create a standard literal
 */
DGStandardLiteral* cdcl_new_standard_literal(cdcl* _cdcl, __uint16_t name, __uint16_t sign){
    DGStandardLiteral* l = new_standard_literal(_cdcl->parentdecision, name, sign);
    (l->literal).implied_by = (DGDecisionLiteral*)_cdcl->parentdecision;
    if(_cdcl->parentdecision != NULL){
        Decision_add_imply((DGDecisionLiteral*)_cdcl->parentdecision, (DGliteral*)l); 
    }
    return l;
}

/**
 * parentdecision <====>  childdecision
 */
DGDecisionLiteral* cdcl_new_decision_literal(cdcl* _cdcl, __uint16_t name, __uint16_t sign){
    DGDecisionLiteral* l = new_decision_literal(name, sign);
    if(_cdcl->parentdecision != NULL){
        literal_add_child(_cdcl->parentdecision, (DGliteral*)l);
        set_add_literal(l->literal.parents, (DGliteral*)_cdcl->parentdecision);
    }
    return l;
}

void cdcl_init(cdcl* _cdcl){
#ifndef MPI_CDCL
    max_var_id++;
#endif    
    _cdcl->parentdecision = NULL;
    _cdcl->dependence_graph = new_graph(); 
    RANKPRINTF(_cdcl->rank, "cdcl init ok");
    //print_graph(_cdcl->dependence_graph);  
}
/**
 * implement SATISFIABLE interface, 
 * call CDCLalgorithm to run the method
 */
_bool cdcl_satisfiable(cnf*_cnf){
    cdcl* _cdcl = malloc(sizeof(cdcl));
    _cdcl->rank = 0;
    _cdcl->round = 0;
    _cdcl->parentdecision = NULL;
    _cdcl->oricnf = _cdcl->_cnf = _cnf;
    _cdcl->config = NULL;
    cdcl_init(_cdcl);
    dpllresult* result = CDCLalgorithm(_cdcl);
    free(_cdcl);
    //printf("try copy result\n");
    print_cnf(result->model_cnf);
    delete_cnf(result->model_cnf);
    return result->sat;
}

/**
 * Adds the neccessary dependency edges to the graph after the unit clause rule was applied
 *
 * The edges are: per previously removed variable in the clause add an edge from the negation
 * of that variable. The negation of the variable is guaranteed to be in the graph.
 * @param name the name of the unit variable
 * @param sign the sign of the unit variable
 * @param clause the unit clause itself
 * 例如 ～@1 ∪ @2 ∪ @3：
 * 3是这次选unit clause选出来的
 * 因此加入 1 ==》3 和 ～2 ==》3 两个依赖路径，注意这里进行了取反
 */
void add_dependency_edges_to_graph(cdcl*_cdcl, __uint16_t name, __uint16_t sign, clause* cls){
    //create new literal and add to graph   
    printf("enter add_dependency_edges_to_graph\n");
    //printf("cls addr %p , try print it\n", &cls);

    DGStandardLiteral* l = new_standard_literal(_cdcl->parentdecision, name, sign);
    DGraph* dependgraph = _cdcl->dependence_graph;
    graph_add_node(dependgraph, (DGliteral*)l);
    assert(cls != NULL);
    //print_clause(cls);
    for(int i = 0; i < cls->var_num; i++){
        if (!(cls->vars[i].name == name && cls->vars[i].sign == sign)){
            //printf("looking for var: %d , sign:%d\n", cls->vars[i].name, cls->vars[i].sign);
            DGliteral* parent = graph_find_negation(dependgraph, &(cls->vars[i]));
            if (parent != NULL){
                if(parent->varname != name){
                    literal_add_child(parent, (DGliteral*)l);
                    set_add_literal(l->literal.parents, parent);
                }
            }else{
                printf("there should exist some node here!\n");
                assert(0);
            }
        }
    }
}

void remove_all_consequences(cdcl* _cdcl, cnf*_cnf,  DGDecisionLiteral* l){
    variable var;
    DGraph* dependence_graph = _cdcl->dependence_graph;
    //printf("%p, remove_all_consequences var %d sign %d\n",_cnf, l->literal.varname, l->literal.varsign);
    //unset value of itself and all consequences
    var.assigned = false;
    for(int i = 0; i < max_var_id * 2; i++){
        if(l->implies->is_in_set[i]){
            var.name = l->implies->literals[i]->varname;
            //printf("unset %d\n", var.name);
            unset_variable_value(_cnf, &var);
        }
    }
    var.name = l->literal.varname;
    //printf("unset %d\n", var.name);
    unset_variable_value(_cnf, &var);
    assert(l->literal.parents != NULL);
    //printf("%p should = %p\n", l->literal.parents, ((DGliteral*)l)->parents);
    assert(((DGliteral*)l)->parents != NULL);
    remove_node(dependence_graph, (DGliteral*)l);
    // for(int i = 0; i < _cnf->nvar; i++){
    //     printf("%d/%d\n", i, _cnf->nvar);
    //     if (_cnf->vars[i].assigned){
    //         DGliteral* l = graph_find(d)
    //     }
    // }
}

void jump_back(cdcl* _cdcl, cnf* _cnf, literal_set* relavant){
    _bool one_popped = false;
    while(_cdcl->parentdecision != NULL){
        //printf("now jump back to %d %d\n", _cdcl->parentdecision->varname, _cdcl->parentdecision->varsign);
        //执行到这俩引起冲突的死掉一个为止
        if (set_find(relavant, _cdcl->parentdecision) != NULL){
            if(one_popped){
                break;
            }
            else{
                one_popped = true;
            }
        }
        assert(_cdcl->parentdecision->parents != NULL);
        remove_all_consequences(_cdcl, _cnf, (DGDecisionLiteral*)_cdcl->parentdecision);

        int parentnum = set_num(_cdcl->parentdecision->parents);
        if(parentnum > 1){
            printf("decision literal's parent num > 0");
            assert(0);
        }
        else if (parentnum == 1){
            _cdcl->parentdecision = set_get_first(_cdcl->parentdecision->parents);
        }else{
            _cdcl->parentdecision = NULL;
        }
    }
}

clause* learn_clause(DGStandardLiteral* pos_literal, DGStandardLiteral* neg_literal){
    queue worklist;
    init_queue(&worklist);
    literal_set* p1 = pos_literal->literal.parents;
    literal_set* p2 = neg_literal->literal.parents;
    assert(p1 != NULL);
    assert(p2 != NULL);
    literal_set* decision_parent = new_literal_set();
    int decision_cnt = 0;
    for(int i = 0; i < max_var_id * 2; i++){
        if(p1->is_in_set[i]){
            //printf("pushed var%d,sign%d\n", p1->literals[i]->varname, p1->literals[i]->varsign);
            push_queue(&worklist, p1->literals[i]);
        }
        if(p2->is_in_set[i]){
            //printf("pushed var%d,sign%d\n", p2->literals[i]->varname, p2->literals[i]->varsign);
            push_queue(&worklist, p2->literals[i]);
        }
    }
    assert(worklist.first != NULL);
    while(worklist.first != NULL){
        assert(worklist.first != NULL);
        DGliteral* l = (DGliteral*)pop_queue(&worklist);
        assert(l != NULL);
        //printf("poped var %d, sign %d\n", l->varname, l->varsign);
        if (l->type == DECISION){
            if (set_find(decision_parent, l) == NULL){
                set_add_literal(decision_parent, l);
            }
            
            //printf("add to decision_parent var %d, sign%d\n", l->varname, l->varsign);

            decision_cnt++;
        }
        else{
            //printf("add var %d, sign %d 's parents to worklist\n", l->varname, l->varsign);
            assert(l->parents != NULL);

            for(int i = 0; i < max_var_id*2; i++){
                if(l->parents->is_in_set[i] > 0){
                    //printf("try add to worklist ,var:%d sign:%d\n", 
                    //l->parents->literals[i]->varname, l->parents->literals[i]->varsign);
                    assert(l->parents->literals[i] != NULL);
                    push_queue(&worklist, l->parents->literals[i]);
                }
            }
        }
    }    
    //printf("make clause\n");
    int index = 0;
    variable* vars = (variable*)malloc(sizeof(variable) * decision_cnt);
    for(int i = 0; i < max_var_id*2; i++){
        if(decision_parent->is_in_set[i]){
            DGliteral* l = decision_parent->literals[i];
            vars[index].name = l->varname;
            vars[index].assigned = 0;
            vars[index].sign = !(l->varsign);
            index++;
        }
    }
    clause* cls = (clause*)malloc(sizeof(clause));
    cls->var_num = index;
    cls->vars = vars;

    free_literal_set(decision_parent);
    return cls;
}

void free_freeable(DGraph* g){
    literal_set* frees = g->free;

    //show free what
    // for(int i = 0; i < 2 * max_var_id; i++){
    //     if(frees->is_in_set[i]){        
    //         DGliteral* l = frees->literals[i];
    //         if (l->type == DECISION) printf("[DEC]");
    //         else printf("[STD]");
    //         printf("%d: var %d, sign %d, addr %p\n", i, l->varname, l->varsign, l);
    //     }
    // }
    for(int i = 0; i < 2 * max_var_id; i++){
        if(frees->is_in_set[i]){
            DGliteral* l = frees->literals[i];
            int type = (l->type == STANDARD) ? 0 : 1;
            
            assert(l->parents != NULL);
            assert(l->children != NULL);
            literal_free(l, type);
            frees->is_in_set[i] = 0;
            frees->literals[i] = NULL;
        }
    }
}

cnf* conflict_resolution(cdcl* _cdcl){
    variable var;
    var.name = _cdcl->dependence_graph->conflict;
    var.sign = 1;
    var.value = 0;
    DGStandardLiteral* pos = (DGStandardLiteral*)graph_find(_cdcl->dependence_graph, &var);
    var.sign = 0;
    DGStandardLiteral* neg = (DGStandardLiteral*)graph_find(_cdcl->dependence_graph, &var);
    clause* newclause = learn_clause(pos, neg);    
    RANKPRINTF(_cdcl->rank, "learned clause %d:\n", _cdcl->_cnf->nclause);
    print_clause(newclause);

    cnf* newcnf = new_cnf_addclause(_cdcl->_cnf, newclause);

    delete_clause(newclause);
    assert(newcnf != _cdcl->oricnf);
    
    literal_set* relavant = new_literal_set();
    assert(pos != neg);
    set_add_literal(relavant, (DGliteral*)pos->literal.implied_by);
    //printf("%d -> %d\n",pos->literal.varname, pos->literal.implied_by->literal.varname);
    //printf("%d -> %d\n",neg->literal.varname, neg->literal.implied_by->literal.varname);

    set_add_literal(relavant, (DGliteral*)neg->literal.implied_by);
    
    //RANKPRINTF(_cdcl->rank, "try jump_back");
    printf("try jump back\n");
    jump_back(_cdcl, newcnf, relavant);
    free_freeable(_cdcl->dependence_graph);
    // printf("free_freeable ok\n");
    _cdcl->dependence_graph->has_conflict = false;
    if(_cdcl->_cnf != _cdcl->oricnf){
        //printf("deleting _cnf %p\n", _cdcl->_cnf);
        delete_cnf(_cdcl->_cnf);
    }
    free_literal_set(relavant);
    return newcnf;
}


extern dpllresult res;
dpllresult* CDCLalgorithm(cdcl* _cdcl){
    variable* var;
    DGraph* dependence_graph = _cdcl->dependence_graph;
    cnf* _cnf = _cdcl->_cnf;
    assert(_cnf != NULL);
    assert(_cdcl != NULL);
    assert(dependence_graph != NULL);
    

    //restart static
    _cdcl->round++;
    if(_cdcl->config != NULL && _cdcl->config->restart_round > 0){
        if (_cdcl->round % _cdcl->config->restart_round == 1){
            RANKPRINTF(_cdcl->rank, "restart");
        }// }
        // else{
        //     RANKPRINTF(_cdcl->rank, "no restart %d mod %d", _cdcl->round, _cdcl->config->restart_round);
        // }
    }
    
    //real conflict that can't continue
    if (dependence_graph->has_conflict && _cdcl->parentdecision == NULL){
        assert(0);
        res.sat = false;
        res.model_cnf = NULL;
        return & res;
    }
    if (dependence_graph->has_conflict){
        printf("conflict happend\n");
        //RANKPRINTF(_cdcl->rank, "conflict happend, try to solve & learn");
        cnf *new_cnf = conflict_resolution(_cdcl);
        assert(dependence_graph->has_conflict == false);
        _cdcl->_cnf = new_cnf;
        //print_cnf(_cdcl->_cnf);
        if (_cdcl->_cnf->nclause < 1000){
            return CDCLalgorithm(_cdcl);
        }
        else return DPLLalgorithm(_cdcl->_cnf);
    }

    if (ALL_CLAUSES_ARE_TRUE(_cnf->clause_set, _cnf->nclause)){
        RANKPRINTF(_cdcl->rank, "found a solution");
        res.sat = true;
        res.model_cnf = _cnf;
        return &res;
    }

    if (ONE_CLAUSE_IS_FALSE(_cnf->clause_set, _cnf->nclause)){
        if (_cdcl->parentdecision == NULL){
            RANKPRINTF(_cdcl->rank, "gg");
            res.sat = false;
            res.model_cnf = NULL;
            return &res;
        }
        else{
            printf("it should have been coped with conflict manager\n");
            assert(0);
        }
    }

    /*optional 可能没啥用*/
    // var = FIND_PURE_VAR(_cnf);
    // if (var != NULL){
    //     printf("pure var %d\n", var->name);
    //     set_variable_value(_cnf, var, var->sign);
    //     return CDCLalgorithm(_cnf);
    // }

    clause* cls;
    _bool seq = 1;
    if (_cdcl->config != NULL){
        seq = _cdcl->config->var_iter;
        //RANKPRINTF(_cdcl->rank, "iter seq %d", seq);
    }

    unit_pair* pair = FIND_UNIT_CLAUSE_P(_cnf, seq);
    if (pair != NULL){
        //RANKPRINTF(_cdcl->rank, "found unit pair: var: %d, sign %d", pair->var->name, pair->var->sign);
        cls = pair->cls;
        var = pair->var;
        assert(cls != NULL);
        assert(var != NULL);
    }
    
    if (pair != NULL && cls != NULL && var != NULL){
        //in this unit clause state
        //a var has to be set to its own sign to
        //SATISFY the clause
        //RANKPRINTF(_cdcl->rank, "unit clause, var %d", var->name);
        //printf("unit clause, var %d", var->name);
        assert(var->name > 0 && var->name < 500);
        //  printf("before enter add dp edge, cls %p\n", cls);
        //print_clause(cls);
        assert(cls->var_num > 0);
        set_variable_value(_cnf, var, var->sign);
        //printf("before enter add dp edge, after print cls\n");
        //printf("before enter add dp edge, after print cls %p\n", cls);

        //add edge to graph.
        add_dependency_edges_to_graph(_cdcl, var->name, var->sign, cls);
        printf("edge added\n");
        //RANKPRINTF(_cdcl->rank, "edge added");
        //print_graph(dependence_graph);
        if (ONE_CLAUSE_IS_FALSE(_cnf->clause_set, _cnf->nclause)){
            //add all edges of FALSE clause
            //this FALSE is caused by var, 
            //we only need to find one false
            clause* false_cls;
            for(int i = 0; i < _cnf->nclause; i++){
                if(clause_is_false(&_cnf->clause_set[i])){
                    false_cls = &_cnf->clause_set[i];
                }
            }
            //adding the false clause to graph will cause "has_conflict"
            add_dependency_edges_to_graph(_cdcl, var->name, !var->sign, false_cls);
            //RANKPRINTF(_cdcl->rank, "conflict edge added");
            //print_graph(dependence_graph);
        } 
        // RANKPRINTF(_cdcl->rank, "free pair %p", pair);
        if (pair != NULL)free(pair);
        printf("free pair ok\n");
        //RANKPRINTF(_cdcl->rank, "free pair ok");
        //this return will cause conflict resolution
        return CDCLalgorithm(_cdcl);
    }

    pair = NULL;
    //normal
    var = find_first_unassigned(_cnf->vars, _cnf->nvar);
    
    if (var == NULL){
        res.model_cnf = NULL;
        res.sat = false;
        //CERR_LEVEL = 0;
        return &res;
    }
    else{        
        //RANKPRINTF(_cdcl->rank, "cdcl decision on %d : %d", var->name, var->value);
        printf("cdcl decision made\n");
        DGDecisionLiteral* dl = cdcl_new_decision_literal(_cdcl, var->name, var->sign); 
        //add to global record
        graph_add_node(dependence_graph, (DGliteral*)dl);

        //print_graph(dependence_graph);
        //record latest decision
        _cdcl->parentdecision = (DGliteral*)dl;

        set_variable_value(_cnf, var, var->sign);
        return CDCLalgorithm(_cdcl);
    }
}